r:, x:. Dec(q-rel(r;x)) 

latex

Definitions

(i = j), qeq(r;s), r * s, qpositive(r), i <z j, b, P & Q, T, P  Q, P  Q, r - s, True, {T}, SQType(T), P  Q, , Dec(P), A, , gset, a < b, goset, a <p b, a < b, t.2, t.1, q_le(r;s), , x f y, <+>, a  b, ff, , tt, P  Q, r < s, r  s, b, p  q, p q, if b then t else f fi , q-rel(r;x), t  T, x:A. B(x), False, Unit, , S  T

Lemmas

bfalse wf, qminus positive, qmul wf, qeq wf2, band wf, member-decide-assert, mon ident q, qadd comm q, qmul zero qrng, qadd wf, true wf, squash wf, btrue wf, int inc rationals, qsub wf, qpositive wf, bool sq, false wf, assert-qeq, not functionality wrt iff, assert of bnot, eqff to assert, not wf, bnot wf, bor wf, ifthenelse wf, assert of eq int, eqtt to assert, assert wf, iff transitivity, bool wf, eq int wf, rationals wf